# Copyright 2024 Google LLC
#
# Licensed under the Apache License, Version 2.0 (the "License");
# you may not use this file except in compliance with the License.
# You may obtain a copy of the License at
#
#      http://www.apache.org/licenses/LICENSE-2.0
#
# Unless required by applicable law or agreed to in writing, software
# distributed under the License is distributed on an "AS IS" BASIS,
# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
# See the License for the specific language governing permissions and
# limitations under the License.

load("//p4_symbolic/symbolic:test.bzl", "end_to_end_test")

package(
    default_visibility = ["//visibility:public"],
    licenses = ["notice"],
)

cc_library(
    name = "v1model_intrinsics",
    hdrs = ["v1model_intrinsic.h"],
)

cc_library(
    name = "operators",
    srcs = ["operators.cc"],
    hdrs = ["operators.h"],
    deps = [
        "//gutil/gutil:status",
        "@com_github_z3prover_z3//:api",
        "@com_google_absl//absl/status",
        "@com_google_absl//absl/status:statusor",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/strings:str_format",
    ],
)

cc_library(
    name = "values",
    srcs = ["values.cc"],
    hdrs = ["values.h"],
    deps = [
        "//gutil/gutil:status",
        "//p4_pdpi:ir_cc_proto",
        "//p4_pdpi/string_encodings:bit_string",
        "//p4_pdpi/utils:ir",
        "//p4_symbolic:z3_util",
        "@com_github_z3prover_z3//:api",
        "@com_gnu_gmp//:gmp",
        "@com_google_absl//absl/container:btree",
        "@com_google_absl//absl/numeric:bits",
        "@com_google_absl//absl/status",
        "@com_google_absl//absl/status:statusor",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/strings:string_view",
    ],
)

cc_library(
    name = "solver_state",
    srcs = [
        "context.cc",
        "deparser.cc",
        "guarded_map.cc",
        "solver_state.cc",
        "symbolic_table_entry.cc",
        "util.cc",
    ],
    hdrs = [
        "context.h",
        "deparser.h",
        "guarded_map.h",
        "solver_state.h",
        "symbolic_table_entry.h",
        "util.h",
    ],
    deps = [
        ":operators",
        ":values",
        "//gutil/gutil:collections",
        "//gutil/gutil:status",
        "//p4_pdpi:ir_cc_proto",
        "//p4_pdpi/internal:ordered_map",
        "//p4_pdpi/string_encodings:bit_string",
        "//p4_symbolic:z3_util",
        "//p4_symbolic/ir",
        "//p4_symbolic/ir:ir_cc_proto",
        "//p4_symbolic/ir:table_entries",
        "@com_github_p4lang_p4runtime//:p4info_cc_proto",
        "@com_github_p4lang_p4runtime//:p4runtime_cc_proto",
        "@com_github_z3prover_z3//:api",
        "@com_google_absl//absl/algorithm:container",
        "@com_google_absl//absl/container:btree",
        "@com_google_absl//absl/container:flat_hash_map",
        "@com_google_absl//absl/log",
        "@com_google_absl//absl/numeric:bits",
        "@com_google_absl//absl/numeric:int128",
        "@com_google_absl//absl/status",
        "@com_google_absl//absl/status:statusor",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/strings:str_format",
        "@com_google_absl//absl/strings:string_view",
        "@com_google_protobuf//:protobuf",
    ],
)

# TODO: Break into separate libraries as much as possible.
cc_library(
    name = "symbolic",
    srcs = [
        "action.cc",
        "conditional.cc",
        "control.cc",
        "parser.cc",
        "symbolic.cc",
        "table.cc",
        "v1model.cc",
    ],
    hdrs = [
        "action.h",
        "conditional.h",
        "control.h",
        "parser.h",
        "symbolic.h",
        "table.h",
        "v1model.h",
    ],
    deps = [
        ":operators",
        ":solver_state",
        ":v1model_intrinsics",
        ":values",
        "//gutil/gutil:collections",
        "//gutil/gutil:status",
        "//p4_pdpi:built_ins",
        "//p4_pdpi:ir_cc_proto",
        "//p4_pdpi/internal:ordered_map",
        "//p4_pdpi/packetlib:packetlib_cc_proto",
        "//p4_symbolic:z3_util",
        "//p4_symbolic/ir",
        "//p4_symbolic/ir:cfg",
        "//p4_symbolic/ir:ir_cc_proto",
        "//p4_symbolic/ir:parser",
        "//p4_symbolic/ir:table_entries",
        "//p4_symbolic/packet_synthesizer:packet_synthesizer_cc_proto",
        "//p4_symbolic/packet_synthesizer:z3_model_to_packet",
        "@com_github_p4lang_p4runtime//:p4info_cc_proto",
        "@com_github_p4lang_p4runtime//:p4runtime_cc_proto",
        "@com_github_z3prover_z3//:api",
        "@com_google_absl//absl/algorithm:container",
        "@com_google_absl//absl/cleanup",
        "@com_google_absl//absl/container:btree",
        "@com_google_absl//absl/log",
        "@com_google_absl//absl/status",
        "@com_google_absl//absl/status:statusor",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/strings:str_format",
        "@com_google_absl//absl/types:optional",
        "@com_google_absl//absl/types:span",
        "@com_google_protobuf//:protobuf",
    ],
)

# Golden file testing rules to test p4_symbolic/main.cc and the SMT
# program generated by p4_symbolic/symbolic/symbolic.cc.
end_to_end_test(
    name = "port_table_test",
    p4_program = "//p4_symbolic/testdata:port-table/table.p4",
    packets_golden_file = "expected/table.txt",
    smt_golden_file = "expected/table.smt2",
    table_entries = "//p4_symbolic/testdata:port-table/entries.pb.txt",
)

end_to_end_test(
    name = "port_hardcoded_test",
    p4_program = "//p4_symbolic/testdata:hardcoded/hardcoded.p4",
    packets_golden_file = "expected/hardcoded.txt",
    smt_golden_file = "expected/hardcoded.smt2",
)

# Checks the behavior of symbolic execution when there is a table application after a conditional.
# Before go/optimized-symbolic-execution, p4-symbolic was executing t3 twice (once from the if
# branch and once from the else branch). Now it executed each table exactly once, leading to
# smaller SMT formulas, hence better constraint solving performance.
end_to_end_test(
    name = "condtional_test",
    p4_program = "//p4_symbolic/testdata:conditional/conditional.p4",
    packets_golden_file = "expected/conditional.txt",
    smt_golden_file = "expected/conditional.smt2",
    table_entries = "//p4_symbolic/testdata:conditional/conditional_entries.pb.txt",
)

end_to_end_test(
    name = "conditional_sequence_test",
    p4_program = "//p4_symbolic/testdata:conditional/conditional_sequence.p4",
    packets_golden_file = "expected/conditional_sequence.txt",
    smt_golden_file = "expected/conditional_sequence.smt2",
    table_entries = "//p4_symbolic/testdata:conditional/conditional_sequence_entries.pb.txt",
)

cc_test(
    name = "values_test",
    srcs = ["values_test.cc"],
    deps = [
        ":values",
        "//gutil/gutil:proto",
        "//gutil/gutil:status_matchers",
        "//p4_pdpi:ir_cc_proto",
        "//p4_symbolic:z3_util",
        "@com_github_z3prover_z3//:api",
        "@com_google_absl//absl/container:flat_hash_map",
        "@com_google_absl//absl/status",
        "@com_google_absl//absl/strings",
        "@com_google_googletest//:gtest_main",
    ],
)

cc_test(
    name = "parser_test",
    srcs = ["parser_test.cc"],
    deps = [
        ":symbolic",
        "//gutil/gutil:proto",
        "//gutil/gutil:status_matchers",
        "//p4_symbolic/ir",
        "//p4_symbolic/ir:ir_cc_proto",
        "@com_github_z3prover_z3//:api",
        "@com_google_absl//absl/container:btree",
        "@com_google_absl//absl/log",
        "@com_google_absl//absl/strings",
        "@com_google_googletest//:gtest_main",
    ],
)

cc_test(
    name = "util_test",
    srcs = ["util_test.cc"],
    deps = [
        ":solver_state",
        "//gutil/gutil:status_matchers",
        "//gutil/gutil:testing",
        "//p4_symbolic/ir:ir_cc_proto",
        "@com_google_absl//absl/status",
        "@com_google_googletest//:gtest_main",
    ],
)

cc_test(
    name = "deparser_test",
    srcs = ["deparser_test.cc"],
    data = [
        "//p4_symbolic/testdata:ipv4-routing/basic.config.json",
        "//p4_symbolic/testdata:ipv4-routing/basic.p4info.pb.txt",
        "//p4_symbolic/testdata:ipv4-routing/entries.pb.txt",
        "//p4_symbolic/testdata:parser/sai_parser.config.json",
        "//p4_symbolic/testdata:parser/sai_parser.p4info.pb.txt",
    ],
    deps = [
        ":solver_state",
        ":symbolic",
        "//gutil/gutil:status_matchers",
        "//p4_pdpi/packetlib",
        "//p4_pdpi/packetlib:packetlib_cc_proto",
        "//p4_symbolic:test_util",
        "@com_github_p4lang_p4runtime//:p4runtime_cc_proto",
        "@com_github_z3prover_z3//:api",
        "@com_google_absl//absl/log",
        "@com_google_absl//absl/status:statusor",
        "@com_google_absl//absl/strings",
        "@com_google_googletest//:gtest_main",
    ],
)

cc_test(
    name = "symbolic_table_entry_test",
    srcs = ["symbolic_table_entry_test.cc"],
    data = [
        "//p4_symbolic/testdata:ipv4-routing/basic.config.json",
        "//p4_symbolic/testdata:ipv4-routing/basic.p4info.pb.txt",
        "//p4_symbolic/testdata:ipv4-routing/entries.pb.txt",
    ],
    deps = [
        ":solver_state",
        ":symbolic",
        "//gutil/gutil:proto_matchers",
        "//gutil/gutil:status",
        "//gutil/gutil:status_matchers",
        "//p4_pdpi:ir_cc_proto",
        "//p4_symbolic:test_util",
        "//p4_symbolic/ir",
        "//p4_symbolic/ir:ir_cc_proto",
        "//p4_symbolic/ir:parser",
        "//p4_symbolic/ir:table_entries",
        "@com_github_p4lang_p4runtime//:p4info_cc_proto",
        "@com_github_p4lang_p4runtime//:p4runtime_cc_proto",
        "@com_github_z3prover_z3//:api",
        "@com_google_absl//absl/status",
        "@com_google_absl//absl/status:statusor",
        "@com_google_absl//absl/strings",
        "@com_google_googletest//:gtest_main",
    ],
)
